$\forall$$i$:Id, $T$:Type, $v$:($\mathbb{Q}\rightarrow$$T$), $x$:Id.
\\[0ex]@$i$: $x$:$T$ initially $x$ = $v$ realizes ${\it es}$. (vartype($i$;$x$) $\subseteq$r $T$) c$\wedge$ (es\_init(${\it es}$)($i$,$x$) = $v$)